//
// THIS FILE IS AUTOMATICALLY GENERATED!!
//
// Generated at Thu 06-Dec-2012 by the VDM++ to JAVA Code Generator
// (v8.0 - Mon 09-Jul-2007 09:32:40)
//
// Supported compilers:
// jdk1.4
//

// ***** VDMTOOLS START Name=HeaderComment KEEP=NO
// ***** VDMTOOLS END Name=HeaderComment

// ***** VDMTOOLS START Name=package KEEP=NO
// ***** VDMTOOLS END Name=package

// ***** VDMTOOLS START Name=imports KEEP=NO

import jp.co.csk.vdm.toolbox.VDM.*;
import java.util.*;
import jp.co.csk.vdm.toolbox.VDM.jdk.*;
// ***** VDMTOOLS END Name=imports



public class Transition implements EvaluatePP {

// ***** VDMTOOLS START Name=vdmComp KEEP=NO
  static UTIL.VDMCompare vdmComp = new UTIL.VDMCompare();
// ***** VDMTOOLS END Name=vdmComp

// ***** VDMTOOLS START Name=startState KEEP=NO
  private volatile State startState = null;
// ***** VDMTOOLS END Name=startState

// ***** VDMTOOLS START Name=endState KEEP=NO
  private volatile State endState = null;
// ***** VDMTOOLS END Name=endState

// ***** VDMTOOLS START Name=name KEEP=NO
  private volatile String name = null;
// ***** VDMTOOLS END Name=name

// ***** VDMTOOLS START Name=sentinel KEEP=NO
  volatile Sentinel sentinel;
// ***** VDMTOOLS END Name=sentinel


// ***** VDMTOOLS START Name=TransitionSentinel KEEP=NO
  class TransitionSentinel extends Sentinel {

    public final int getName = 0;

    public final int Transition = 1;

    public final int getEndState = 2;

    public final int getStartState = 3;

    public final int nr_functions = 4;


    public TransitionSentinel () throws CGException {}


    public TransitionSentinel (EvaluatePP instance) throws CGException {
      init(nr_functions, instance);
    }

  }
// ***** VDMTOOLS END Name=TransitionSentinel
;

// ***** VDMTOOLS START Name=evaluatePP KEEP=NO
  public Boolean evaluatePP (int fnr) throws CGException {
    return new Boolean(true);
  }
// ***** VDMTOOLS END Name=evaluatePP


// ***** VDMTOOLS START Name=setSentinel KEEP=NO
  public void setSentinel () {
    try {
      sentinel = new TransitionSentinel(this);
    }
    catch (CGException e) {
      System.out.println(e.getMessage());
    }
  }
// ***** VDMTOOLS END Name=setSentinel


// ***** VDMTOOLS START Name=Transition KEEP=NO
  public Transition () throws CGException {
    try {
      setSentinel();
    }
    catch (Exception e){

      e.printStackTrace(System.out);
      System.out.println(e.getMessage());
    }
  }
// ***** VDMTOOLS END Name=Transition


// ***** VDMTOOLS START Name=Transition KEEP=NO
  public Transition (final String n, final State starts, final State ends) throws CGException {

    try {
      setSentinel();
    }
    catch (Exception e){

      e.printStackTrace(System.out);
      System.out.println(e.getMessage());
    }
    {

      name = UTIL.ConvertToString(UTIL.clone(n));
      startState = (State) UTIL.clone(starts);
      endState = (State) UTIL.clone(ends);
    }
  }
// ***** VDMTOOLS END Name=Transition


// ***** VDMTOOLS START Name=getStartState KEEP=NO
  public State getStartState () throws CGException {

    sentinel.entering(((TransitionSentinel) sentinel).getStartState);
    try {
      return (State) startState;
    }
    finally {
      sentinel.leaving(((TransitionSentinel) sentinel).getStartState);
    }
  }
// ***** VDMTOOLS END Name=getStartState


// ***** VDMTOOLS START Name=getEndState KEEP=NO
  public State getEndState () throws CGException {

    sentinel.entering(((TransitionSentinel) sentinel).getEndState);
    try {
      return (State) endState;
    }
    finally {
      sentinel.leaving(((TransitionSentinel) sentinel).getEndState);
    }
  }
// ***** VDMTOOLS END Name=getEndState


// ***** VDMTOOLS START Name=getName KEEP=NO
  public String getName () throws CGException {

    sentinel.entering(((TransitionSentinel) sentinel).getName);
    try {
      return name;
    }
    finally {
      sentinel.leaving(((TransitionSentinel) sentinel).getName);
    }
  }
// ***** VDMTOOLS END Name=getName

}
;
